Nuprl Lemma : qmul-qdiv-cancel3
11,40
postcript
pdf
a
,
b
,
c
:
. (
(
a
= 0
))
((
a
* (
b
/
a
) *
c
) = (
b
*
c
)
)
latex
Definitions
T
,
P
&
Q
,
P
Q
,
P
Q
,
True
,
,
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
S
T
Lemmas
qmul-qdiv-cancel
,
true
wf
,
squash
wf
,
qmul
assoc
,
qmul
wf
,
qdiv
wf
,
int
inc
rationals
,
rationals
wf
,
not
wf
origin
a, b, c:
. (
(a = 0 
)) 
((a * (b/a) * c) = (b * c) ) a, b, c:. ((a = 0 )) ((a * (b/a) * c) = (b * c) ) 
T
Q Q
T Qx:A. B(x)
T